/* s2 - find first zero byte with clz
   Copyright (C) 2018 Ariadne Devos

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   (at your option) any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. */

#include <sHT/bitops.h>
#include <stdint.h>

_Static_assert(sHT_word_zero_index_prepare(UINT64_C(23)) == ~UINT64_C(23), "inconsitent with <sHT/bitops.h>");

/* noinline is for benchmarking */
__attribute__((noinline))
int
sHT_word_zero_index64(uint64_t word)
{
	/* @var{word} has been inverted, so search for a 255 byte instead
	   of nul. To do that, first correct the byte border, secondly &
	   all bits of a byte together, lastly search for the most significant
	   set bit. */
	word = sHT_htobe64(word);
	/* Bring the bits to the left.
	   i is the i'th bit, starting from the most significant.
	   E@i is the value of the E'th bit in the i'th state.
	   The state starts at 0, and increments after each statement. */

	/* i@1 := i@0 & (i + 1)@0. */
	word &= word << 1;
	/* i@2 := i@1 & (i + 2)@1. */
	word &= word << 2;
	/* i@3 := i@2 & (i + 4)@2. */
	word &= word << 4;
	/* Proof of correctness of these ampersands:

	  Start with i@3, and expand until everything is written in terms
	  of i@0. Apply associativity of addition and compute addition
	  of constants after each expansion. Take note that & is associative.

	  (i)@3
	  = (i)@2 & (i + 4)@2
	  = (i)@1 & (i + 2)@1 & (i + 4)@1 & (i + 6)@1
	  = (i)@0 & (i + 1)@0 & (i + 2)@0 & (i + 3)@0
	    & (i + 4)@0 & (i + 5)@0 & (i + 6)@0 & (i + 7)

	  Eight subsequent bits are and together into the first.
	  But we're not done yet: 8i + 1 may still be set.
	  Apply a bitmask. */
	/*@ 8i@4 := 8i@3, (8i + 0...7)@3 := 0 */
	word &= 0x8080808080808080;
	/* Replace 8i@4 with its definition ==> first bit is correct.
	   (8i + 0...7)@3 is correct by definition (zero). */
	/* There are 8 bits in a byte. */
	return sHT_clz64(word) / 8;
}

